package com.googlecode.kipler.syntax.formula;

import com.googlecode.kipler.syntax.LTLUnaryOperator;


public class LTLUnaryFormula extends Formula {

	private LTLUnaryOperator constructor;

	private Formula operand;

	public LTLUnaryFormula() {

	}

	public LTLUnaryFormula(LTLUnaryOperator constructor, Formula operand) {
		super();
		this.constructor = constructor;
		this.operand = operand;
	}

	public LTLUnaryOperator getConstructor() {
		return constructor;
	}

	public void setConstructor(LTLUnaryOperator constructor) {
		this.constructor = constructor;
	}

	public Formula getOperand() {
		return operand;
	}

	public void setOperand(Formula operand) {
		this.operand = operand;
	}

	@Override
	public boolean isNegated() {
		return false;
	}

	@Override
	public Formula toggleNegated() {
		if (getConstructor().equals(LTLUnaryOperator.SOMETIME)) {
			setConstructor(LTLUnaryOperator.ALWAYS);
		} else if (getConstructor().equals(LTLUnaryOperator.ALWAYS)) {
			setConstructor(LTLUnaryOperator.SOMETIME);
		}
		// nothing to do for next operator
		setOperand(getOperand().toggleNegated());
		return this;
	}

	@Override
	public boolean equals(Object obj) {
		if (obj != null && (obj.getClass().equals(this.getClass()))) {
			LTLUnaryFormula other = (LTLUnaryFormula) obj;
			return (this.getConstructor().equals(other.getConstructor()) && this
					.getOperand().equals(other.getOperand()));
		}
		return false;
	}

	@Override
	public int hashCode() {
		return 17 * 37 + super.hashCode() + getConstructor().hashCode()
				+ getOperand().hashCode();
	}

	public LTLUnaryFormula copy() {
		LTLUnaryFormula result = new LTLUnaryFormula();
		result.setConstructor(getConstructor());
		result.setOperand(getOperand().copy());
		return result;
	}

	/**
	 * @see java.lang.Object#toString()
	 */
	@Override
	public String toString() {
		StringBuffer buffer = new StringBuffer();
		buffer.append(getConstructor());
		buffer.append("(");
		buffer.append(getOperand());
		buffer.append(")");
		return buffer.toString();
	}

	@Override
	public void accept(FormulaVisitor v) {
		v.visitLTLUnaryFormula(this);
	}

}
